I'm not sure I get what the goal is here. Its because we are already showing the most simplified version in the refinement error that we don't need the other values?

I'm especially confused about the 2nd example, its very weird that we show #a_2 == X and not #a_1. Should we also be removing #a_2 since it is nowhere in the simplified error message?

Also, it raises a question, should we just present the simplified error version in the console version? in the ide we can expand it but here could be helpful to also present the full-on error message to match the counterexample.

(unrelated but these errors will be much better when we apply #162 )

This is not really about filtering out assignments that are not present in the simplified expression of the error message, but about filtering out the assignments that are already present in the context. This change resulted from a conversation with @alcides, where we agreed that if the context already includes a refinement shown in the counterexample, we consider it redundant and remove it to simplify the counterexample.

Regarding showing unsimplified expressions in the command-line version, maybe we could add a command argument like --no-simplification to do so, but I think always showing both versions would be too verbose.

The main point is:

void f(@Refined("x > 0") int x) {
   int a = 3;
   f(x - a);
}

In this case, the counter example showing that a == 3 is not very useful, because it was assigned before (there may be thousands of variables in the body, including those from anf). We care about the x, because its refinement is not an equality, so a proper witness matters.

Does this make sense? or am I missing some other case, where showing other variables (we know about) is relevant?

We already do a filtering of the context refinements sent to the smt solver for each check, so we should only get the relevant variables in the counter example right

It’s different. We are talking about formulas that are relevant for type-checking but do not add anything new to what the programmer already knows.

if they know a = 3 but b > 0, the counter example of b will be relevant, but the counter example of a will be 3, as expected from the source code.

Yes, if we send the refinement x = 1 to the SMT solver, x = 1 appearing in the counterexample is just not useful.

Ok but still you are assuming that the developer remembers that x = 1, and it's not too far away in the program from the place the error shows up.
I think we could have 2 options for both the refinement found and the counter example: 1) simplified version, and 2) with the complete information. In the IDE we can hide it and reveal after upon need, but in the text message we can start by having the simplified version and then a bar with the complete info or something

@alcides because of the concerns that @CatarinaGamboa raised, instead of filtering out assignments in the counterexample that are already present in the context, we now filter out assignments of variables that don't appear in the error message, which actually shows better results than the previous approach.

You're right, I overlooked that detail.